【buu】[GXYCTF2019]simple CPP

这题主要是分析函数，就是 CPP 反编译后的那一坨有点绕

也是看了别的师傅的 wp 才慢慢理解

put_in

这里是动调后才知道这个函数是输入，把函数名字更改更好理解

下面的 if 判断语句中的 **v40 - 5 > 25 **已经表明了输入的字符长度不能超过 30

然后是一段意义不明的函数段

接着到了这里

xor_encry

这里也有一些意义不明

动调发现，v41 和 qword_7FF7A0466060 都百年成了 0x1F

所以 v9 的值就是输入的 flag

走完循环后 v10 就变成了 i_will_check_is_debug_or_not

v12

v6 就是输入的 flag 和 v10 进行逐步异或

赋值

这也是有点抽象 v43 上面已经说了不能超过 30

而这里给了个 if ( (int)v43 > 30 )和 if ( (int)v43 <= 0 )

否则会前往表示 flag 格式错误的语句

看正确情况下的赋值语句，这里是将输入的 flag 每 8 位分成一组，分别赋值给 v14，v13，v12，v11，这里 v11 只有 4 位前三个都是 8 位

下面有一小段没有截图截到

那是把 v14，v13，v12，v11 又赋值给 v18[0]，v18[1]，v18[2]，v18[3]

赋值2与密文

正确的情况下是不会走 lable_27 的

所以应该是走 lable_28

这里是一大串赋值与运算操作

关键部分是那几个 if 语句

用 z3 约束求解器把

求完的值拼起来追溯到头就是 flag 和 v10 异或后的值

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
from z3 import*
v0 = BitVec('v0', 64)
v1 = BitVec('v1', 64)
v2 = BitVec('v2', 64)
v3 = BitVec('v3', 64)

s = Solver()
#添加约束条件
s.add(v2 & ~v0 == 1176889593874)
s.add((v2 & ~v1) & v0 | v2 & ((v1 & v0) | v1 & ~v0 | ~(v1 | v0)) == 577031497978884115)
s.add((v2 & ~v0) | (v1 & v0) | (v2 & ~v1) | (v0 & ~v1) == 4483974544037412639)
s.add(((v2 & ~v0) | (v1 & v0) | (v2 & ~v1) | (v0 & ~v1))^v3 == 4483974543195470111)
s.add(((v2 & ~v0) | (v1 & v0) | v1 & v2) == (~v0 & v2 | 864693332579200012))

# 检查是否有解
if s.check() == sat:
    # 如果有解，打印模型
    print("6666")
    # print chr
    m = s.model()
    print("v0 =", hex(m[v0].as_long()))
    print("v1 =", hex(m[v1].as_long()))
    print("v2 =", hex(m[v2].as_long()))
    print("v3 =", hex(m[v3].as_long()))
else:
    print("No solution exists")

然后拼起来和 v10 进行异或就是 flag

1
2
3
4
5
6
enc = [0x3e,0x3a,0x46,0x05,0x33,0x28,0x6f,0x0d,0xc,0x00,0x02,0x01,0x30,0x08,0x2c,0x0c,0x8,0x02,0x07,0x17,0x15,0x3e,0x30,0x13,0x32,0x31,0x06,0x00]
v12 = 'i_will_check_is_debug_or_not'
flag =''
for i in range(len(enc)-1):
    flag += chr(ord(v12[i%27]) ^ enc[i])
print(flag)

这里程序执行完会发现不对

原题这里给了段 hint 第二组数据为 e!P0or_a，但是 buu 没有给

所以只要把相应部位换成 e!P0or_a 即可